T:Type, f:(TT), L1, L2:(T List), x, y, z:T.
z=f*(x) via L1 @ [y / L2]  {y=f*(x) via [y / L2] & z=f*(y) via L1 @ [y]} 

latex

Definitions	type List, t  T, s = t, Type, x:AB(x), y=f*(x) via L, , x:A  B(x), P & Q, {T}, P  Q, x:A. B(x), [], A List, [car / cdr], P  Q, P  Q, a < b, hd(l), {i..j}, A, #$n, i <z j, i z j, l[i], last(L), as @ bs, s ~ t, ||as||, , A  B, i  j , Void, False, t  ...$L, f(a)
Lemmas	hd wf, length nil, length cons, non neg length, length append, length wf1, fun-path-cons, append wf, not wf, int seg wf, guard wf, fun-path wf, iff wf